UVa/12315 - The Starflyer Agents/ana.cpp

   1 using namespace std;
   2 #include <algorithm>
   3 #include <iostream>
   4 #include <iterator>
   5 #include <numeric>
   6 #include <sstream>
   7 #include <fstream>
   8 #include <cassert>
   9 #include <climits>
  10 #include <cstdlib>
  11 #include <cstring>
  12 #include <string>
  13 #include <cstdio>
  14 #include <vector>
  15 #include <cmath>
  16 #include <queue>
  17 #include <deque>
  18 #include <stack>
  19 #include <list>
  20 #include <map>
  21 #include <set>
  22
  23 #define foreach(x, v) for (typeof (v).begin() x=(v).begin(); x !=(v).end(); ++x)
  24 #define For(i, a, b) for (int i=(a); i<(b); ++i)
  25 #define D(x) cout << #x " is " << x << endl
  26
  27 bool doUnify;
  28
  29 bool isFunctor(string hash){
  30         int n = hash.size();
  31         if (n <= 3) return false;
  32         if (hash[0] < 'a' || hash[0] >'z') return false;
  33         for (int i = 1; i < n; i++){
  34                 if (hash[i] == '('){
  35                         return true;
  36                 }
  37                 if (hash[i] == ','){
  38                         return false;
  39                 }
  40         }
  41         return false;
  42 }
  43
  44 string getFun(string hash){
  45         int n = hash.size();
  46         string ans = "";
  47         for (int i = 0; i < n; i++){
  48                 if (hash[i] == '(') break;
  49                 ans += hash[i];
  50         }
  51         return ans;
  52 }
  53 vector <string> getArgs (string hash){
  54         int n = hash.size();
  55         vector <string> args;
  56         string arg = "";
  57         bool paren = false;
  58
  59         queue <char> p;
  60         for (int i = 0; i < n - 1; i++){
  61                 if (hash[i] == ')'){
  62                         p.pop();
  63                 }
  64
  65                 if (hash[i] == ',' && p.size() == 0){
  66                         args.push_back(arg);
  67                         arg = "";
  68                 }else{
  69                         if(paren) arg += hash[i];
  70                 }
  71
  72                 if (hash[i] == '('){
  73                         if (!paren){
  74                                 paren = true;
  75                         }else{
  76                                 p.push('(');
  77                         }
  78                 }
  79                 if (i == n - 2) args.push_back(arg);
  80         }
  81         return args;
  82 }
  83
  84 bool isVar(string hash){
  85         if(hash[0] < 'A' || hash[0] > 'Z') return false;
  86         return true;
  87 }
  88
  89 bool isConst(string hash){
  90         if (isVar(hash) || isFunctor(hash)) return false;
  91         return true;
  92 }
  93
  94 bool occurs(string var, string hash){
  95         if (hash.find(var) == string::npos) return false;
  96         return true;
  97 }
  98
  99 vector<pair<string, string> > unify (string hash1, string hash2){
 100         vector <pair<string, string> > ans;
 101         // Verify if they already unify
 102         if (!doUnify) return ans;
 103
 104         int n1 = hash1.size();
 105         int n2 = hash2.size();
 106         if (n1 == 0 || n2 == 0) return ans;
 107         // Unify functors
 108         if (isFunctor(hash1) and isFunctor(hash2)){
 109                 if (getFun(hash1) == getFun(hash2)){
 110                         //Unify arguments
 111                         vector <string> v1 = getArgs(hash1);
 112                         vector <string> v2 = getArgs(hash2);
 113                         if (v1.size() != v2.size()){
 114                                 doUnify = false;
 115                                 return ans;
 116                         }
 117                         for (int i = 0; i < v1.size(); i++){
 118                                 vector <pair<string, string> > vect = unify(v1[i], v2[i]);
 119                                 if (!doUnify) return ans;
 120                                 for (int j = 0; j < vect.size(); j++){
 121                                         ans.push_back(vect[j]);
 122                                 }
 123                         }
 124                 }else{
 125                         doUnify = false;
 126                         return ans;
 127                 }
 128         }else{
 129                 // Unify variable and constant
 130                 if(isVar(hash1) && isConst(hash2)){
 131                         ans.push_back(make_pair(hash1, hash2));
 132                         return ans;
 133                 }
 134                 if(isVar(hash2) && isConst(hash1)){
 135                         ans.push_back(make_pair(hash2, hash1));
 136                         return ans;
 137                 }
 138                 // Unify variable and variable/ functor
 139                 if(isVar(hash1) and !isConst(hash2)){
 140                         if (occurs(hash1, hash2)){
 141                                 if(hash1 == hash2) return ans;
 142                                 doUnify = false;
 143                                 return ans;
 144                         }
 145                         ans.push_back(make_pair(hash1, hash2));
 146                         return ans;
 147                 }
 148                 if(isVar(hash2) and !isConst(hash1)){
 149                         if (occurs(hash2, hash1)){
 150                                 doUnify = false;
 151                                 return ans;
 152                         }
 153                         ans.push_back(make_pair(hash2, hash1));
 154                         return ans;
 155                 }
 156                 // Unify two constants
 157                 if (isConst(hash1) && isConst(hash2)){
 158                         if(hash1 != hash2) doUnify = false;
 159                         return ans;
 160                 }
 161                 // Unify a constant and a functor
 162                 doUnify = false;
 163                 return ans;
 164         }
 165         return ans;
 166 }
 167 string replce(string oc, string str, string rep){
 168         while(str.find(oc) != string::npos){
 169                 int pos = str.find(oc);
 170                 str.replace(pos, oc.size(), rep);
 171         }
 172         return str;
 173 }
 174
 175 vector<pair<string, string> > make_replacements( vector<pair<string,string> > v ){
 176         int n = v.size();
 177         for (int i = 0; i < n; i++){
 178                 string var = v[i].first;
 179                 string rep = v[i].second;
 180                 for (int j = 0; j < n; j++){
 181                         if (j == i) continue;
 182                         //If the variable is in the first term
 183                         if (v[j].first == var){
 184                                 string second = v[j].second;
 185                                 if (!isVar(second)){
 186                                         v.erase (v.begin()+j);
 187                                         //Erase it and add the unification of the other varibles
 188                                         vector<pair<string, string> > unif = unify(rep, second);
 189                                         for (int k = 0; k < unif.size(); k++){
 190                                                 v.push_back(unif[k]);
 191                                         }
 192                                 }else if(!isVar(rep)){
 193                                         v[j].second = rep;
 194                                         v[j].first = second;
 195                                 }else{
 196                                         v[j].first = rep;
 197                                 }
 198                         }
 199                         //If the variable is in the second term
 200                         if (occurs(var, v[j].second) ){
 201                                 if (occurs(v[j].first, rep)){
 202                                         doUnify = false;
 203                                         return v;
 204                                 }
 205                                 v[j].second = replce(var, v[j].second, rep);
 206                         }
 207                         if (!doUnify) break;
 208                 }
 209                 if (!doUnify) break;
 210         }
 211         return v;
 212 }
 213
 214
 215 int main(){
 216         string name;
 217         int n;
 218
 219         //CHEQUEO
 220         /*doUnify = true;
 221         vector< pair<string, string> > v = unify("f(f(X),Z)","f(f(Y), c)");
 222         for (int i = 0; i < v.size(); i++){
 223                 printf("%s / %s\n", v[i].first.c_str(), v[i].second.c_str());
 224         }*/
 225
 226         while (cin >> name >> n){
 227                 if (n == 0) break;
 228                 string hash [n];
 229                 for (int i = 0; i < n; i++) cin >> hash[i];
 230
 231         vector<pair<string, string> > unifiers [n - 1];
 232
 233         for (int i = 0; i < n - 1; i++){
 234                 doUnify = true;
 235                 unifiers[i] = unify(hash[i], hash[i+1]);
 236                 //Make replacements with unifiers
 237                 if (doUnify) unifiers[i] = make_replacements(unifiers[i]);
 238                 if (!doUnify) break;
 239         }
 240         /*for (int i = 0; i < n - 1; i++){
 241                 int n = unifiers[i].size();
 242                 printf("El unificador %d es:\n", i);
 243                 for (int j = 0; j < n; j++){
 244                         printf("%s / %s\n", (unifiers[i][j].first).c_str(), (unifiers[i][j].second).c_str());
 245                 }
 246         }*/
 247         if (doUnify){
 248                 vector <pair<string, string> > joint = unifiers[0];
 249                 for (int i = 1; i < n - 1; i++){
 250                         for (int k = 0; k < unifiers[i].size(); k++){
 251                                 for (int j = 0; j < joint.size(); j++){
 252                                         // Make replacement
 253                                         if (occurs(unifiers[i][k].first, joint[j].second)){
 254                                                 if(occurs(joint[j].first, unifiers[i][k].second) ){
 255                                                         doUnify = false;
 256                                                         break;
 257                                                 }else{
 258                                                         joint[j].second = replce( unifiers[i][k].first, joint[j].second, unifiers[i][k].second );
 259                                                 }
 260                                         }
 261                                 }
 262                                 if (!doUnify) break;
 263                                 for (int j = 0; j < joint.size(); j++){
 264                                         if(unifiers[i][k].first == joint[j].first){
 265                                                 unifiers[i].erase(unifiers[i].begin()+k);
 266                                                 break;
 267                                         }
 268                                 }
 269                         }
 270                         if (!doUnify) break;
 271                         for (int k = 0; k < unifiers[i].size(); k++){
 272                                 joint.push_back(unifiers[i][k]);
 273                         }
 274                         int n = joint.size();
 275                         /*printf("El unificador %d conjunto es:\n", i);
 276                         for (int j = 0; j < n; j++){
 277                                 printf("%s / %s\n", (joint[j].first).c_str(), (joint[j].second).c_str());
 278                         }*/
 279                 }
 280         }
 281
 282         if (!doUnify){
 283                 printf("%s is a Starflyer agent\n", name.c_str());
 284         }else{
 285                 printf("analysis inconclusive on %s\n", name.c_str());
 286         }
 287
 288
 289         }
 290     return 0;
 291 }